es:ES, e:E, l:IdLnk, tg:Id.
(e sends on l with tag tg)  (loc(es-first-from(es;e;l;tg)) ~ destination(l)) 

latex

Definitions	ES, t  T, x:A. B(x), E, IdLnk, Id, (e sends on l with tag tg), destination(l), loc(e), <a, b>, s = t, {T}, P  Q, SQType(T), s ~ t, True, isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), b, isrcv(e), x:A  B(x), t.1, Atom$n, P & Q, es-first-from(es;e;l;tg), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), lnk(e)
Lemmas	es-axioms, es-kind-first-from, Id sq, es-sends-on wf, Id wf, IdLnk wf, es-E wf, event system wf